T:Type, f:(TT), x, y:T. (x = y)  y is f*(x) 

latex

Definitions	Type, t  T, s = t, x:AB(x), , x:A  B(x), x:A. B(x), x:A. B(x), type List, y=f*(x) via L, P  Q, y is f*(x), A List, [], [car / cdr], {i..j}, #$n, A, n+m, l[i], f(a), P & Q, a < b, Void, False, A  B, i  j , t  ...$L, ||as||, , hd(l), i <z j, i z j, last(L)
Lemmas	length nil, length cons, non neg length, length wf1, not wf, int seg wf, fun-path wf